Nuprl Lemma : ma-single-pre-true-feasible
0,22
postcript
pdf
a
:Id. Feasible(precondition
a
: True)
latex
Definitions
x
:
A
.
B
(
x
)
,
Feasible(
M
)
,
precondition
a
: True
,
mk-ma
,
,
x
:
v
,
P
&
Q
,
x
dom(
f
).
v
=
f
(
x
)
P
(
x
;
v
)
,
1of(
t
)
,
2of(
t
)
,
f
(
x
)?
z
,
M
.frame(
k
affects
x
)
,
P
Q
,
M
.sframe(
k
sends <
l
,
tg
>)
,
b
,
x
dom(
f
)
,
f
(
x
)
,
if
b
t
else
f
fi
,
z
!=
f
(
x
)
P
(
a
;
z
)
,
deq-member(
eq
;
x
;
L
)
,
reduce(
f
;
k
;
as
)
,
false
,
Y
,
t
T
,
x
.
t
(
x
)
,
Dec(
P
)
,
x
:
A
.
B
(
x
)
,
Top
,
True
,
P
Q
,
Prop
,
False
,
x
(
s
)
Lemmas
false
wf
,
Id
wf
,
Knd
wf
,
ma-state
wf
,
fpf-empty
wf
,
assert
wf
,
bor
wf
,
eqof
wf
,
id-deq
wf
,
bfalse
wf
,
IdLnk
wf
,
true
wf
,
not
wf
,
top
wf
origin
a:Id. Feasible(precondition a: True) a:Id. Feasible(precondition a: True) x:A. B(x)x
dom(f). v=f(x) 
P(x;v) Q
b dom(f)
t else f fi P(a;z)
T
x. t(x)
x:A. B(x)
Q